T:Type, j:, l:T List. 0<j  j<||l||  ((firstn(j-1;l) @ [l[j-1]]) ~ firstn(j;l)) 

latex

Definitions	P  Q, x:A. B(x), t  T, Prop, ||as||, {T}, SQType(T), l[i], as @ bs, , ij, False, A, AB, P  Q, Dec(P), tl(l), hd(l), i<j, ij, P  Q, P & Q, P  Q, True, b, b, , T, Unit
Lemmas	bnot of le int, squash wf, true wf, bool wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, bnot of lt int, assert of le int, lt int wf, le int wf, le wf, assert wf, bnot wf, length tl, tl wf, list decomp, decidable int equal, ge wf, nat properties, nat wf, length wf1